Thierry Coquand

Thierry Coquand
Thierry Coquand en 2006
Información personal
Nacimiento	18 de abril de 1961 (63 años) Isère (Francia)
Nacionalidad	Francesa
Educación
Educación	doctor en Filosofía
Educado en	Escuela Normal Superior de París
Supervisor doctoral	Gérard Huet
Información profesional
Ocupación	Matemático, informático teórico e ingeniero
Área	Ciencias de la computación
Empleador	Universidad de Gotemburgo Universidad Politécnica de Chalmers Institut National de Recherche en Informatique et en Automatique
Obras notables	Coq
Miembro de	Academia Europæa (desde 2011)
Distinciones	ACM Software System Award (2013)
[editar datos en Wikidata]

Thierry Coquand (pronunciación en francés: /kɔkɑ̃/; Bourgoin-Jallieu, 18 de abril de 1961) es un informático y matemático francés que actualmente es profesor de informática en la Universidad de Gotemburgo,^[1]​ habiendo trabajado anteriormente en INRIA. Es conocido por su trabajo en matemáticas constructivas, especialmente el cálculo de construcciones.

Recibió su Ph.D. bajo la supervisión de Gérard Huet, otro académico con experiencia tanto en matemáticas como en informática. Según la biblioteca digital ACM, su primer artículo publicado fue una colaboración de 1985 con Huet titulada «Construcciones: un sistema de prueba de orden superior para mecanizar las matemáticas».^[2]​ Coquand y Huet publicaron otro artículo conjunto en septiembre de ese año que amplió aún más sus ideas sobre las matemáticas constructivas.^[3]​ Al año siguiente, 1986, Coquand publicó un artículo notable sobre la paradoja de Girard en el sistema lógico Sistema U.^[4]​ Desde entonces, Coquand ha escrito una amplia variedad de artículos tanto en francés como en inglés.

Además de sus contribuciones a la informática teórica, Coquand también es conocido por ser el cocreador del asistente de prueba Coq (el nombre es en parte una referencia al apellido de Coquand), cuyo desarrollo comenzó en 1984 mientras trabajaba en INRIA (el Instituto Nacional de Investigación de Ciencias de la Computación y Matemáticas de Francia), y que se lanzó oficialmente en 1989.^[5]​ Coq ganó el premio de software de lenguajes de programación SIGPLAN ACM en 2013 por «proporcionar un entorno rico para el desarrollo interactivo del razonamiento formal verificado por máquina».^[6]​^[7]​ Coq se ha utilizado para proporcionar soluciones novedosas para problemas matemáticos, especialmente para aquellos que tienen una prueba no comprobable, como el teorema de los cuatro colores. También se ha utilizado en el desarrollo de software, como con el compilador CompCert C.^[8]​

Coquand a menudo da charlas sobre los temas en los que se especializa, como su descripción del trabajo del profesor de la Universidad de Nottingham Thorsten Altenkirch.^[9]​

1. ↑ «Thierry Coquand» (en inglés). Universidad de Gotemburgo. Archivado desde el original el 27 de marzo de 2023. Consultado el 27 de marzo de 2023. 
2. ↑ Constructions: A Higher Order Proof System for Mechanizing Mathematics (en inglés). Abril de 1985. pp. 151-184. ISBN 9783540159834. Consultado el 24 de febrero de 2023. 
3. ↑ Coquand, Thierry; Huet, Gérard (1985). «A Selected Bibliography on Constructive Mathematics, Intuitionistic Type Theory and Higher Order Deduction». Journal of Symbolic Computation (en inglés) 1 (3): 323-328. doi:10.1016/S0747-7171(85)80040-7. Archivado desde el original el 24 de febrero de 2023. Consultado el 24 de febrero de 2023. 
4. ↑ «An analysis of Girard's paradox» (en inglés). Archivado desde el original el 24 de febrero de 2023. Consultado el 24 de febrero de 2023. 
5. ↑ «What is Coq?» (en inglés). Archivado desde el original el 24 de febrero de 2023. Consultado el 24 de febrero de 2023. 
6. ↑ «Coq received ACM SIGPLAN Programming Languages Software 2013 award» (en inglés). Archivado desde el original el 22 de febrero de 2023. Consultado el 22 de febrero de 2023. 
7. ↑ «Programming Languages Software Award» (en inglés). Archivado desde el original el 25 de febrero de 2023. Consultado el 25 de febrero de 2023. 
8. ↑ «Thierry Coquand» (en inglés). Archivado desde el original el 25 de febrero de 2023. Consultado el 25 de febrero de 2023. 
9. ↑ «Paradoxes and Definitions» (en inglés). Archivado desde el original el 25 de febrero de 2023. Consultado el 25 de febrero de 2023.